\begin{tabbing}
$\forall$${\it es}$:ES, $i$:Id, $L$:IdLnk List, $T$:(Id$\rightarrow$Type).
\\[0ex]es{-}secret{-}server\=\{table:ut2, encrypt:ut2, decrypt:ut2\}\+
\\[0ex](${\it es}$; $T$; $L$; $i$)
\-\\[0ex]$\Rightarrow$ (\=$\forall$$e_{1}$, $e_{2}$:E.\+
\\[0ex]($\exists$$l$$\in$$L$.kind($e_{1}$) $=$ rcv(lnk{-}inv($l$),"encrypt") $\in$ Knd)
\\[0ex]$\Rightarrow$ ($\exists$$l$$\in$$L$.kind($e_{2}$) $=$ rcv(lnk{-}inv($l$),"encrypt") $\in$ Knd)
\\[0ex]$\Rightarrow$ 2of(val($e_{1}$)) $=$ 2of(val($e_{2}$)) $\in$ Atom1
\\[0ex]$\Rightarrow$ $e_{1}$ $=$ $e_{2}$)
\-
\end{tabbing}